package be.jas.mvc.base;


import be.jas.generated.FeatureType;
import be.jas.generated.Perspective;
import be.jas.generated.Productline;
import be.jas.mvc.base.model.CombinationIterator;
import be.jas.mvc.base.model.fam.FamComposition;
import be.jas.mvc.base.model.fam.FamFeature;
import be.jas.mvc.base.model.fam.FamManager;
import be.jas.mvc.base.model.fam.FamPerspective;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.*;
import org.springframework.stereotype.Service;

import javax.xml.bind.JAXBContext;
import javax.xml.bind.JAXBElement;
import javax.xml.bind.JAXBException;
import javax.xml.bind.Unmarshaller;
import java.io.File;
import java.io.PrintWriter;
import java.util.*;

/**
 * Created with IntelliJ IDEA.
 * User: jasmien
 * Date: 2/07/13
 * Time: 9:34
 * To change this template use File | Settings | File Templates.
 */
@Service
public class MyPerspectiveService implements PerspectiveService {

    private static final int MAXVAR = 1000;
    private static final int NBCLAUSES = 5000;
    private static final int TIMEOUT = 60; //# of seconds


    private FamFeature createFeature(FeatureType featureType, FamManager manager, List<FamFeature> parentFeatures, FamPerspective famPerspective, FamComposition composition){
        FamFeature feature = new FamFeature(featureType.getId(), featureType.getName());
        feature.setConcrete("concrete".equals(featureType.getType()));
        //Add to global and perspective
        manager.addFeature(feature);
        famPerspective.addFeature(feature);
        for(FamFeature parent : parentFeatures){
            parent.addFeature(feature);
        }
        //Add to FamManager and FamFeature  (default values)

        //Add to composition for "rules" later on
        if(composition != null){
            composition.addFeature(feature);
        }
        return feature;
    }

    /*
        Process XML and generate all basic features
     */
    private FamFeature ProcessFeature(FeatureType featureType, FamManager manager, List<FamFeature> parentFeatures, FamPerspective famPerspective){
        return ProcessFeature(featureType, manager, parentFeatures, famPerspective, null);
    }

    private FamFeature ProcessFeature(FeatureType featureType, FamManager manager, List<FamFeature> parentFeatures, FamPerspective famPerspective, FamComposition composition){
        FamFeature feature = createFeature(featureType, manager, parentFeatures, famPerspective, composition);
        parentFeatures.add(feature);
        for (Object o : featureType.getContent()) {
            if (o instanceof JAXBElement) {
                JAXBElement el = (JAXBElement) o;
                if (el.getValue() instanceof FeatureType.OptionalComposition) {
                    FamComposition optComp = feature.addOptionalComposition();
                    FeatureType.OptionalComposition oc = (FeatureType.OptionalComposition) el.getValue();
                    for (FeatureType subFT : oc.getFeature()) {
                        ProcessFeature(subFT, manager, parentFeatures, famPerspective, optComp);
                    }
                } else if (el.getValue() instanceof FeatureType.MandatoryComposition) {
                    FamComposition manComp = feature.addMandatoryComposition();
                    FeatureType.MandatoryComposition mc = (FeatureType.MandatoryComposition) el.getValue();
                    for (FeatureType subFT : mc.getFeature()) {
                        ProcessFeature(subFT, manager, parentFeatures, famPerspective, manComp);
                    }
                } else if(el.getValue() instanceof FeatureType.Option) {
                        FeatureType.Option option = (FeatureType.Option) el.getValue();
                        for (FeatureType subFT : option.getFeature()) {
                            ProcessFeature(subFT, manager, parentFeatures, famPerspective);
                        }
                }
            }
        }
        parentFeatures.remove(feature);
        return feature;
    }

    /*
        Process xml for a 2nd time to retrieve all the features using their reference in restrictions
     */
    private FamFeature ProcessFeature2(FeatureType featureType, FamManager manager){
        FamFeature feature = manager.getFeature(featureType.getId());
        System.out.println("Processing feature: " + featureType.getId());
        for (Object o : featureType.getContent()) {
            if (o instanceof JAXBElement) {
                JAXBElement el = (JAXBElement) o;
                if (el.getValue() instanceof FeatureType.OptionalComposition) {
                    FeatureType.OptionalComposition oc = (FeatureType.OptionalComposition) el.getValue();
                    for (FeatureType subFT : oc.getFeature()) {
                        ProcessFeature2(subFT, manager);
                    }
                } else if (el.getValue() instanceof FeatureType.MandatoryComposition) {
                    FeatureType.MandatoryComposition mc = (FeatureType.MandatoryComposition) el.getValue();
                    for (FeatureType subFT : mc.getFeature()) {
                        ProcessFeature2(subFT, manager);
                    }
                } else if(el.getValue() instanceof FeatureType.Option) {
                    FeatureType.Option option = (FeatureType.Option) el.getValue();
                    for (FeatureType subFT : option.getFeature()) {
                        ProcessFeature2(subFT, manager);
                    }
                } else if(el.getValue() instanceof  FeatureType) { //Restriction!!
                    System.out.println("Name: " + el.getName() + ", Class: " + el.getValue().getClass().getName());

                    if("requires".equals(el.getName().getLocalPart())){
                        feature.addRequires(manager.getFeature(((FeatureType)el.getValue()).getId()));
                    } else  if("excludes".equals(el.getName().getLocalPart())){
                        feature.addExclude(manager.getFeature(((FeatureType)el.getValue()).getId()));
                    } else  if("same".equals(el.getName().getLocalPart())){
                        feature.addSame(manager.getFeature(((FeatureType)el.getValue()).getId()));
                    } else  if("incompatible".equals(el.getName().getLocalPart())){
                        feature.addIncompatible(manager.getFeature(((FeatureType)el.getValue()).getId()));
                    } else  if("uses".equals(el.getName().getLocalPart())){
                        feature.addUses(manager.getFeature(((FeatureType)el.getValue()).getId()));
                    } else  if("includes".equals(el.getName().getLocalPart())){
                        feature.addIncludes(manager.getFeature(((FeatureType)el.getValue()).getId()));
                    } else  if("impacts".equals(el.getName().getLocalPart())){
                        feature.addImpacts(manager.getFeature(((FeatureType)el.getValue()).getId()));
                    } else  if("extends".equals(el.getName().getLocalPart())){
                        feature.addExtends(manager.getFeature(((FeatureType)el.getValue()).getId()));
                    }
                } else if(el.getValue() instanceof FeatureType.Cardinality) {
                    FeatureType.Cardinality card = (FeatureType.Cardinality) el.getValue();
                    feature.setCardinality(card.getMin(), card.getMax());
                } else if ("description".equals(el.getName().getLocalPart())){
                    feature.setDescription(el.getValue().toString());
                } else {
                    System.out.println("Other element" + el.getValue() + "/" + el.getValue().getClass().getName() + "/" + el.getName() + "\n");
                }
            }
        }
        return feature;
    }



    @Override
    public FamManager generateStoreFromFile(File file) {
        FamManager manager = new FamManager();
        try {
            JAXBContext c = JAXBContext.newInstance(new Class[]{Productline.class});
            Unmarshaller um = c.createUnmarshaller();
            Productline pl = (Productline) um.unmarshal(file);

            for (Perspective p : pl.getPerspective()) {

                System.out.println("Perspective: " + p.getName());

                FamPerspective famPerspective = new FamPerspective(p.getName(), p.getDescription());
                manager.addPerspective(famPerspective);

                //Step 1: get the features
                for (FeatureType ft : p.getFeature()) {
                    ProcessFeature(ft, manager, new ArrayList<FamFeature>(), famPerspective);
                }

                //Step 2: loop again over the tree and make the necessary restrictions and relationships between the features
                for (FeatureType featureType : p.getFeature()) {
                    ProcessFeature2(featureType, manager);
                }

            }
            //System.out.println(manager);
            System.out.println(manager.getFeature("f4").toString("\t"));

        } catch (JAXBException e) {
            // TODO Auto-generated catch block
            e.printStackTrace();
        }
        return manager;
    }

    @Override
    public List<String> ValidateRules(FamManager manager, FamPerspective perspective) {
        List<String> errors = new ArrayList<String>();
//        try {
            ISolver managerSolver = SolverFactory.newDefault();
            managerSolver.setTimeout(TIMEOUT); // 60 second timeout
            // prepare the managerSolver to accept MAXVAR variables. MANDATORY for MAXSAT solving
            managerSolver.newVar(MAXVAR);
            managerSolver.setExpectedNumberOfClauses(NBCLAUSES);

            ISolver perspectiveSolver = SolverFactory.newDefault();
            perspectiveSolver.setTimeout(TIMEOUT); // 60 second timeout
            // prepare the managerSolver to accept MAXVAR variables. MANDATORY for MAXSAT solving
            perspectiveSolver.newVar(MAXVAR);
            perspectiveSolver.setExpectedNumberOfClauses(NBCLAUSES);
            //TODO regels

            for(FamFeature famFeature : perspective.getFeatures()){
                errors.addAll(solveFeature(famFeature, perspectiveSolver, managerSolver, new ArrayList<FamFeature>()));
            }

            //TODO add solving for manager and perspective
//        } catch (TimeoutException e) {
//            errors.add("global timeout while checking!");
//        } catch (ContradictionException e) {
//            errors.add("global has a contradiction in it's rules!");
//        }
        return errors;
    }

    private List<String> solveFeature(FamFeature feature, ISolver persolver, ISolver mansolver, List<FamFeature> checkedFeatures){
        List<String> errors = new ArrayList<String>();
        if(!checkedFeatures.contains(feature)) {
            try{
               checkedFeatures.add(feature);


                //Prepare solver
                ISolver solver = SolverFactory.newDefault();
                solver.setTimeout(TIMEOUT); // 60 second timeout
                // prepare the solver to accept MAXVAR variables. MANDATORY for MAXSAT solving
                solver.newVar(MAXVAR);
                solver.setExpectedNumberOfClauses(NBCLAUSES);

                //retrieve all subfeatures
                Collection<FamFeature> allFeatures = feature.getAllFeatures();
                List<FamFeature> options = feature.getFeatures();
                //Add Rules
                if(feature.isValue()){



                    //Check if subrules are valid
                    for(FamFeature subfeature : options){
                        errors.addAll(solveFeature(subfeature, persolver, mansolver, checkedFeatures));
                    }

                    if(!areCombinationsValid(feature)){
                        errors.add(feature.getName() + " cardinality is invalid!");
                    }

                    for(FamComposition composition : feature.getCompositions()){
                        //Check if subrules are valid
                        for(FamFeature subfeature : composition.getFeatures()){
                            errors.addAll(solveFeature(subfeature, persolver, mansolver, checkedFeatures));
                            //If mandatory check if the subfeatures are selected
                            if(composition.getMandatory()){
                                VecInt mandatory = new VecInt(1);
                                mandatory.push(subfeature.getIndex()); //TODO rekening houden met same!! => or opbouwen?
                                solver.addClause(mandatory);
                            }
                        }
                    }

                    for(FamFeature requires : feature.getRequires()){
                        IVecInt required = new VecInt(1);
                        required.push(requires.getIndex());
                        solver.addClause(required);
                    }

                    for(FamFeature excludes : feature.getExcludes()){
                        IVecInt excl = new VecInt(1);
                        excl.push(-excludes.getIndex());
                        solver.addClause(excl);
                    }

                    //TODO 8 constraints


                } else {
                    if(!allFeatures.isEmpty()){
                        VecInt allNull = new VecInt(allFeatures.size());
                        for(FamFeature subfeature : allFeatures){
                            allNull.push(-subfeature.getIndex());
                        }
                        solver.addClause(allNull);
                    }
                }

                //Assume values
                List<FamFeature> ftWithConstraints = feature.getAllFeaturesWithConstraints();
                VecInt solution = new VecInt(ftWithConstraints.size());
                for(FamFeature subfeature : ftWithConstraints){
                    solution.push(subfeature.isValue() ? subfeature.getIndex() : -subfeature.getIndex());
                }

                IProblem problem = solver;
                if (!problem.isSatisfiable(solution) || !errors.isEmpty()) {
                    errors.add(feature.getName() + " is unsatisfied!");
                }
            } catch (TimeoutException e) {
                errors.add(feature.getName() + " timeout while checking!");
            } catch (ContradictionException e) {
                errors.add(feature.getName() + " has a contradiction in it's rules!");
            }
        }
        return errors;
    }

    private boolean areCombinationsValid(FamFeature feature) throws ContradictionException, TimeoutException {
        List<FamFeature> options = feature.getFeatures();
        boolean found_result = options.isEmpty();
        boolean found_invalid_result = false;
        int max = feature.getMax() < options.size() ? feature.getMax() + 1 : feature.getMax();
        for(int size = feature.getMin(); size < max; size++){

            CombinationIterator<FamFeature> iterator = new CombinationIterator<FamFeature>(options, size);
            while(iterator.hasNext() && !found_invalid_result){

                List<FamFeature> combination = iterator.next();
                VecInt comb = new VecInt(combination.size());
                VecInt solution = new VecInt(combination.size());

                for(FamFeature subfeature : combination){
                    comb.push(subfeature.getIndex());
                    solution.push(subfeature.isValue() ? subfeature.getIndex() : -subfeature.getIndex());
                }

                //Prepare solver
                ISolver solver = SolverFactory.newDefault();
                solver.setTimeout(TIMEOUT); // 60 second timeout
                // prepare the solver to accept MAXVAR variables. MANDATORY for MAXSAT solving
                solver.newVar(MAXVAR);
                solver.setExpectedNumberOfClauses(NBCLAUSES);

                solver.addClause(comb);
                if(solver.isSatisfiable(solution)){
                    if(size < feature.getMin() || size > feature.getMax()){
                        found_invalid_result = true;
                    } else {
                        found_result = true;
                    }
                }

            }
            if(found_invalid_result)
                break;
        }
        return found_result && !found_invalid_result;
    }


}
